Left Termination of the query pattern
ackerman(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 183 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 173 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 PiDPToQDPProof (⇒, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 PiDP
        ↳13 PiDPToQDPProof (⇒, 0 ms)
        ↳14 QDP
        ↳15 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

Clauses:

ackerman(0, N, s(N)).
ackerman(s(M), 0, Res) :- ackerman(M, s(0), Res).
ackerman(s(M), s(N), Res) :- ','(ackerman(s(M), N, Res1), ackerman(M, Res1, Res)).

Query: ackerman(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

ackermanB(X1, X2) :- ackermanC(X1, X2).
ackermanC(s(X1), X2) :- ackermanB(X1, X3).
ackermanC(s(X1), X2) :- ','(ackermancB(X1, X3), ackermanD(X1, X3, X2)).
ackermanD(s(X1), 0, X2) :- ackermanC(X1, X2).
ackermanD(s(X1), s(X2), X3) :- ackermanD(s(X1), X2, X4).
ackermanD(s(X1), s(X2), X3) :- ','(ackermancD(s(X1), X2, X4), ackermanD(X1, X4, X3)).
ackermanA(s(s(X1)), 0, X2) :- ackermanB(X1, X3).
ackermanA(s(s(X1)), 0, X2) :- ','(ackermancB(X1, X3), ackermanA(X1, X3, X2)).
ackermanA(s(X1), s(0), X2) :- ackermanC(X1, X3).
ackermanA(s(X1), s(0), X2) :- ','(ackermancC(X1, X3), ackermanA(X1, X3, X2)).
ackermanA(s(X1), s(s(X2)), X3) :- ackermanD(s(X1), X2, X4).
ackermanA(s(X1), s(s(X2)), X3) :- ','(ackermancD(s(X1), X2, X4), ackermanD(X1, X4, X5)).
ackermanA(s(X1), s(s(X2)), X3) :- ','(ackermancD(s(X1), X2, X4), ','(ackermancD(X1, X4, X5), ackermanA(X1, X5, X3))).

Clauses:

ackermancA(0, X1, s(X1)).
ackermancA(s(0), 0, s(s(0))).
ackermancA(s(s(X1)), 0, X2) :- ','(ackermancB(X1, X3), ackermancA(X1, X3, X2)).
ackermancA(s(X1), s(0), X2) :- ','(ackermancC(X1, X3), ackermancA(X1, X3, X2)).
ackermancA(s(X1), s(s(X2)), X3) :- ','(ackermancD(s(X1), X2, X4), ','(ackermancD(X1, X4, X5), ackermancA(X1, X5, X3))).
ackermancB(X1, X2) :- ackermancC(X1, X2).
ackermancC(0, s(s(0))).
ackermancC(s(X1), X2) :- ','(ackermancB(X1, X3), ackermancD(X1, X3, X2)).
ackermancD(0, X1, s(X1)).
ackermancD(s(X1), 0, X2) :- ackermancC(X1, X2).
ackermancD(s(X1), s(X2), X3) :- ','(ackermancD(s(X1), X2, X4), ackermancD(X1, X4, X3)).

Afs:

ackermanA(x1, x2, x3)  =  ackermanA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermanA_in: (b,b,f)
ackermanB_in: (b,f)
ackermanC_in: (b,f)
ackermancB_in: (b,f)
ackermancC_in: (b,f)
ackermancD_in: (b,b,f)
ackermanD_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermanB_in_ga(X1, X3))
ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANB_IN_GA(X1, X3)
ACKERMANB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermanC_in_ga(X1, X2))
ACKERMANB_IN_GA(X1, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMANC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermanB_in_ga(X1, X3))
ACKERMANC_IN_GA(s(X1), X2) → ACKERMANB_IN_GA(X1, X3)
ACKERMANC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermancB_in_ga(X1, X3))
U3_GA(X1, X2, ackermancB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermanD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMAND_IN_GGA(X1, X3, X2)
ACKERMAND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermanC_in_ga(X1, X2))
ACKERMAND_IN_GGA(s(X1), 0, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermanD_in_gga(s(X1), X2, X4))
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → ACKERMAND_IN_GGA(s(X1), X2, X4)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermanD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4, X3)
ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermancB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermancB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermanA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermanC_in_ga(X1, X3))
ACKERMANA_IN_GGA(s(X1), s(0), X2) → ACKERMANC_IN_GA(X1, X3)
ACKERMANA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermancC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermancC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermanA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermancC_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermanD_in_gga(s(X1), X2, X4))
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMAND_IN_GGA(s(X1), X2, X4)
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermanD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermancD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermancD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermanA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermancD_out_gga(X1, X4, X5)) → ACKERMANA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermancB_in_ga(X1, X2) → U28_ga(X1, X2, ackermancC_in_ga(X1, X2))
ackermancC_in_ga(0, s(s(0))) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermancB_in_ga(X1, X3))
U29_ga(X1, X2, ackermancB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermancD_in_gga(X1, X3, X2))
ackermancD_in_gga(0, X1, s(X1)) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermancC_in_ga(X1, X2))
U31_gga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermancD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackermanA_in_gga(x1, x2, x3)  =  ackermanA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackermanB_in_ga(x1, x2)  =  ackermanB_in_ga(x1)
ackermanC_in_ga(x1, x2)  =  ackermanC_in_ga(x1)
ackermancB_in_ga(x1, x2)  =  ackermancB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermancC_in_ga(x1, x2)  =  ackermancC_in_ga(x1)
ackermancC_out_ga(x1, x2)  =  ackermancC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermancB_out_ga(x1, x2)  =  ackermancB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermancD_in_gga(x1, x2, x3)  =  ackermancD_in_gga(x1, x2)
ackermancD_out_gga(x1, x2, x3)  =  ackermancD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackermanD_in_gga(x1, x2, x3)  =  ackermanD_in_gga(x1, x2)
ACKERMANA_IN_GGA(x1, x2, x3)  =  ACKERMANA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKERMANB_IN_GA(x1, x2)  =  ACKERMANB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANC_IN_GA(x1, x2)  =  ACKERMANC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMAND_IN_GGA(x1, x2, x3)  =  ACKERMAND_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermanB_in_ga(X1, X3))
ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANB_IN_GA(X1, X3)
ACKERMANB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermanC_in_ga(X1, X2))
ACKERMANB_IN_GA(X1, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMANC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermanB_in_ga(X1, X3))
ACKERMANC_IN_GA(s(X1), X2) → ACKERMANB_IN_GA(X1, X3)
ACKERMANC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermancB_in_ga(X1, X3))
U3_GA(X1, X2, ackermancB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermanD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMAND_IN_GGA(X1, X3, X2)
ACKERMAND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermanC_in_ga(X1, X2))
ACKERMAND_IN_GGA(s(X1), 0, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermanD_in_gga(s(X1), X2, X4))
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → ACKERMAND_IN_GGA(s(X1), X2, X4)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermanD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4, X3)
ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermancB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermancB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermanA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermanC_in_ga(X1, X3))
ACKERMANA_IN_GGA(s(X1), s(0), X2) → ACKERMANC_IN_GA(X1, X3)
ACKERMANA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermancC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermancC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermanA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermancC_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermanD_in_gga(s(X1), X2, X4))
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMAND_IN_GGA(s(X1), X2, X4)
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermanD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermancD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermancD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermanA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermancD_out_gga(X1, X4, X5)) → ACKERMANA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermancB_in_ga(X1, X2) → U28_ga(X1, X2, ackermancC_in_ga(X1, X2))
ackermancC_in_ga(0, s(s(0))) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermancB_in_ga(X1, X3))
U29_ga(X1, X2, ackermancB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermancD_in_gga(X1, X3, X2))
ackermancD_in_gga(0, X1, s(X1)) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermancC_in_ga(X1, X2))
U31_gga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermancD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackermanA_in_gga(x1, x2, x3)  =  ackermanA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackermanB_in_ga(x1, x2)  =  ackermanB_in_ga(x1)
ackermanC_in_ga(x1, x2)  =  ackermanC_in_ga(x1)
ackermancB_in_ga(x1, x2)  =  ackermancB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermancC_in_ga(x1, x2)  =  ackermancC_in_ga(x1)
ackermancC_out_ga(x1, x2)  =  ackermancC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermancB_out_ga(x1, x2)  =  ackermancB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermancD_in_gga(x1, x2, x3)  =  ackermancD_in_gga(x1, x2)
ackermancD_out_gga(x1, x2, x3)  =  ackermancD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackermanD_in_gga(x1, x2, x3)  =  ackermanD_in_gga(x1, x2)
ACKERMANA_IN_GGA(x1, x2, x3)  =  ACKERMANA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKERMANB_IN_GA(x1, x2)  =  ACKERMANB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANC_IN_GA(x1, x2)  =  ACKERMANC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMAND_IN_GGA(x1, x2, x3)  =  ACKERMAND_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANB_IN_GA(X1, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMANC_IN_GA(s(X1), X2) → ACKERMANB_IN_GA(X1, X3)
ACKERMANC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermancB_in_ga(X1, X3))
U3_GA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMAND_IN_GGA(X1, X3, X2)
ACKERMAND_IN_GGA(s(X1), 0, X2) → ACKERMANC_IN_GA(X1, X2)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → ACKERMAND_IN_GGA(s(X1), X2, X4)
ACKERMAND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4, X3)

The TRS R consists of the following rules:

ackermancB_in_ga(X1, X2) → U28_ga(X1, X2, ackermancC_in_ga(X1, X2))
ackermancC_in_ga(0, s(s(0))) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermancB_in_ga(X1, X3))
U29_ga(X1, X2, ackermancB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermancD_in_gga(X1, X3, X2))
ackermancD_in_gga(0, X1, s(X1)) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermancC_in_ga(X1, X2))
U31_gga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermancD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackermancB_in_ga(x1, x2)  =  ackermancB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermancC_in_ga(x1, x2)  =  ackermancC_in_ga(x1)
ackermancC_out_ga(x1, x2)  =  ackermancC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermancB_out_ga(x1, x2)  =  ackermancB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermancD_in_gga(x1, x2, x3)  =  ackermancD_in_gga(x1, x2)
ackermancD_out_gga(x1, x2, x3)  =  ackermancD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKERMANB_IN_GA(x1, x2)  =  ACKERMANB_IN_GA(x1)
ACKERMANC_IN_GA(x1, x2)  =  ACKERMANC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
ACKERMAND_IN_GGA(x1, x2, x3)  =  ACKERMAND_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANB_IN_GA(X1) → ACKERMANC_IN_GA(X1)
ACKERMANC_IN_GA(s(X1)) → ACKERMANB_IN_GA(X1)
ACKERMANC_IN_GA(s(X1)) → U3_GA(X1, ackermancB_in_ga(X1))
U3_GA(X1, ackermancB_out_ga(X1, X3)) → ACKERMAND_IN_GGA(X1, X3)
ACKERMAND_IN_GGA(s(X1), 0) → ACKERMANC_IN_GA(X1)
ACKERMAND_IN_GGA(s(X1), s(X2)) → ACKERMAND_IN_GGA(s(X1), X2)
ACKERMAND_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackermancD_in_gga(s(X1), X2))
U7_GGA(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4)

The TRS R consists of the following rules:

ackermancB_in_ga(X1) → U28_ga(X1, ackermancC_in_ga(X1))
ackermancC_in_ga(0) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1)) → U29_ga(X1, ackermancB_in_ga(X1))
U29_ga(X1, ackermancB_out_ga(X1, X3)) → U30_ga(X1, ackermancD_in_gga(X1, X3))
ackermancD_in_gga(0, X1) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0) → U31_gga(X1, ackermancC_in_ga(X1))
U31_gga(X1, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermancD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermancD_in_gga(X1, X4))
U33_gga(X1, X2, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The set Q consists of the following terms:

ackermancB_in_ga(x0)
ackermancC_in_ga(x0)
U29_ga(x0, x1)
ackermancD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACKERMANC_IN_GA(s(X1)) → ACKERMANB_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • ACKERMANC_IN_GA(s(X1)) → U3_GA(X1, ackermancB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKERMANB_IN_GA(X1) → ACKERMANC_IN_GA(X1)
    The graph contains the following edges 1 >= 1

  • ACKERMAND_IN_GGA(s(X1), 0) → ACKERMANC_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • U3_GA(X1, ackermancB_out_ga(X1, X3)) → ACKERMAND_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U7_GGA(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → ACKERMAND_IN_GGA(X1, X4)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKERMAND_IN_GGA(s(X1), s(X2)) → ACKERMAND_IN_GGA(s(X1), X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ACKERMAND_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackermancD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermancB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermancB_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermancC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermancC_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3, X2)
ACKERMANA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermancD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermancD_out_gga(X1, X4, X5)) → ACKERMANA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermancB_in_ga(X1, X2) → U28_ga(X1, X2, ackermancC_in_ga(X1, X2))
ackermancC_in_ga(0, s(s(0))) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermancB_in_ga(X1, X3))
U29_ga(X1, X2, ackermancB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermancD_in_gga(X1, X3, X2))
ackermancD_in_gga(0, X1, s(X1)) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermancC_in_ga(X1, X2))
U31_gga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermancD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermancD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackermancB_in_ga(x1, x2)  =  ackermancB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermancC_in_ga(x1, x2)  =  ackermancC_in_ga(x1)
ackermancC_out_ga(x1, x2)  =  ackermancC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermancB_out_ga(x1, x2)  =  ackermancB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermancD_in_gga(x1, x2, x3)  =  ackermancD_in_gga(x1, x2)
ackermancD_out_gga(x1, x2, x3)  =  ackermancD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKERMANA_IN_GGA(x1, x2, x3)  =  ACKERMANA_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackermancB_in_ga(X1))
U10_GGA(X1, ackermancB_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3)
ACKERMANA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackermancC_in_ga(X1))
U13_GGA(X1, ackermancC_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3)
ACKERMANA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackermancD_in_gga(s(X1), X2))
U16_GGA(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackermancD_in_gga(X1, X4))
U18_GGA(X1, X2, ackermancD_out_gga(X1, X4, X5)) → ACKERMANA_IN_GGA(X1, X5)

The TRS R consists of the following rules:

ackermancB_in_ga(X1) → U28_ga(X1, ackermancC_in_ga(X1))
ackermancC_in_ga(0) → ackermancC_out_ga(0, s(s(0)))
ackermancC_in_ga(s(X1)) → U29_ga(X1, ackermancB_in_ga(X1))
U29_ga(X1, ackermancB_out_ga(X1, X3)) → U30_ga(X1, ackermancD_in_gga(X1, X3))
ackermancD_in_gga(0, X1) → ackermancD_out_gga(0, X1, s(X1))
ackermancD_in_gga(s(X1), 0) → U31_gga(X1, ackermancC_in_ga(X1))
U31_gga(X1, ackermancC_out_ga(X1, X2)) → ackermancD_out_gga(s(X1), 0, X2)
ackermancD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermancD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermancD_in_gga(X1, X4))
U33_gga(X1, X2, ackermancD_out_gga(X1, X4, X3)) → ackermancD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermancD_out_gga(X1, X3, X2)) → ackermancC_out_ga(s(X1), X2)
U28_ga(X1, ackermancC_out_ga(X1, X2)) → ackermancB_out_ga(X1, X2)

The set Q consists of the following terms:

ackermancB_in_ga(x0)
ackermancC_in_ga(x0)
U29_ga(x0, x1)
ackermancD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U10_GGA(X1, ackermancB_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • ACKERMANA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackermancB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • U16_GGA(X1, X2, ackermancD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackermancD_in_gga(X1, X4))
    The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2, 3 > 2

  • U13_GGA(X1, ackermancC_out_ga(X1, X3)) → ACKERMANA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U18_GGA(X1, X2, ackermancD_out_gga(X1, X4, X5)) → ACKERMANA_IN_GGA(X1, X5)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKERMANA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackermancC_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKERMANA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackermancD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(16) YES